Nuprl Lemma : alle-rcv_wf
11,40
postcript
pdf
es
:ES,
l
:IdLnk,
tg
:Id,
P
:({
e
:E|
isrcv(
e
)}
). (
e
=rcv(
l
,
tg
).
P
(
e
))
latex
Definitions
ES
,
t
T
,
IdLnk
,
Id
,
,
x
:
A
.
B
(
x
)
,
isrcv(
e
)
,
b
,
E
,
x
(
s
)
,
rcv(
l
,
tg
)
,
kind(
e
)
,
Knd
,
P
Q
,
e
=rcv(
l
,
tg
).
P
(
e
)
,
True
,
isrcv(
k
)
,
{
T
}
,
SQType(
T
)
Lemmas
Knd
sq
,
Knd
wf
,
es-kind
wf
,
rcv
wf
,
es-E
wf
,
assert
wf
,
es-isrcv
wf
,
Id
wf
,
IdLnk
wf
,
event
system
wf
origin
es:ES, l:IdLnk, tg:Id, P:({e:E| 
isrcv(e)} 
). (e=rcv(l,tg). P(e)) 
es:ES, l:IdLnk, tg:Id, P:({e:E| isrcv(e)} ). (e=rcv(l,tg). P(e)) Tx:A. B(x)b
Qe=rcv(l,tg). P(e)